Nuprl Lemma : es-send_wf
11,40
postcript
pdf
es
:event_system{i:l},
i
:Id.
es-send(
es
;
i
)
k
:Knd
es-kindtype(
es
;
i
;
k
)
es-state(
es
;
i
)
(es-Msg(
es
) List)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
Msg(
M
)
,
type
List
,
f
(
a
)
,
Id
,
x
:
A
B
(
x
)
,
tag(
k
)
,
lnk(
k
)
,
act(
k
)
,
islocal(
k
)
,
isrcv(
k
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
))
,
x
:
A
B
(
x
)
,
left
+
right
,
Knd
,
Type
,
if
b
then
t
else
f
fi
,
x
.
A
(
x
)
,
b
,
P
Q
,
IdLnk
,
x
,
y
.
t
(
x
;
y
)
,
x
.
t
(
x
)
,
P
Q
,
es-T(
es
)
,
es-Send(
es
)
,
es-M(
es
)
,
es-vartype(
es
;
i
;
x
)
,
es-V(
es
)
,
es-send(
es
;
i
)
,
es-Msg(
es
)
,
es-state(
es
;
i
)
,
es-kindtype(
es
;
i
;
k
)
,
event_system{i:l}
Lemmas
event
system
wf
,
subtype
rel
dep
function
,
kindcase
wf
,
IdLnk
wf
,
ifthenelse
wf
,
isrcv
wf
,
lnk
wf
,
tagof
wf
,
actof
wf
,
Knd
wf
,
subtype
rel
self
,
Id
wf
,
Msg
wf
origin
es:event_system{i:l}, i:Id.
k:Knd
es-kindtype(es; i; k)es-state(es; i)(es-Msg(es) List) es:event_system{i:l}, i:Id.
k:Kndes-kindtype(es; i; k)es-state(es; i)(es-Msg(es) List) 
B(x)
x.A(x)
b
Q
x,y. t(x;y)
Q